COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST RW ε WORLD
C00007 ENDMK
C⊗;
declare INDCONST RW ε WORLD;
declare INDVAR w w1 w2 w3 w4 w5 ε WORLD;
declare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

declare OPCONST arab(NATNUM) = PERSON;
declare INDVAR p p0 p1 p2 ε PERSON;
declare INDCONST Gossip ε PERSON;
declare PREDCONST human(PERSON);

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

declare INDVAR c c1 c2 c3 c4 ε WIFESTATES;
declare INDCONST FAITHFUL UNFAITHFUL ε WIFESTATES;

declare OPCONST wifestate(PERSON,WORLD) = WIFESTATES;

axiom reflex:	∀w p m.A(w,w,p,m);;

axiom transitive:	∀w1 w2 w3 p m.(A(w1,w2,p,m) ∧ A(w2,w3,p,m) ⊃ A(w1,w3,p,m));;

axiom wifestate:	¬FAITHFUL=UNFAITHFUL
			∀c.(c=FAITHFUL ∨ c=UNFAITHFUL)
;;

axiom who:	∀p.(human(p) ∨ p=Gossip)
		¬human(Gossip)
;;

axiom gossip:	∀w1 w2 p m.(A(w1,w2,p,m) ⊃ A(w1,w2,Gossip,m));;

axiom rw:	card {pεPERSON | wifestate(p,RW) = UNFAITHFUL} = 40;;

axiom initial:	∀c w.(A(RW,w,Gossip,0) ⊃
	∀p.(human(p) ∧ (c=UNFAITHFUL ∨ ∃p1.(¬p1=p ∧ wifestate(p1,w1)
							= UNFAITHFUL))
		⊃ ∃w1.(A(w,w1,p,0) ∧ wifestate(p,w1) = c))

	∀w w1 p p1.(A(RW,w,Gossip,0) ∧ A(w,w1,p,0) ∧ ¬(p=p1)
		⊃ wifesstate(p1,w1) = wifestate(p1,w))
;;

axiom caliph:	∀w.(A(RW,w,W123,0) ⊃ ∃p.(human(p) ∧ wifestate(p)=UNFAITHFUL));;

axiom elwek:	∀w m.(A(RW,w,Gossip,m+1) ≡ A(RW,w,Gossip,m) ∧
	∀p.(human(p) ⊃
		(∀w1.(A(w,w1,p,m) ⊃ wifestate(p,w1)=wifestate(p,w))
		≡ ∀w1.(A(RW,w1,p,m) ⊃ wifestate(p,w1)=wifestate(p,RW)))))

	∀w1 w2 p.(A(w1,w2,p,m+1) ≡ A(w1,w2,p,m) ∧ A(w1,w2,Gossip,m+1))
;;